1: | a__incr(nil) | → nil | |
2: | a__incr(cons(X,L)) | → cons(s(mark(X)),incr(L)) | |
3: | a__adx(nil) | → nil | |
4: | a__adx(cons(X,L)) | → a__incr(cons(mark(X),adx(L))) | |
5: | a__nats | → a__adx(a__zeros) | |
6: | a__zeros | → cons(0,zeros) | |
7: | a__head(cons(X,L)) | → mark(X) | |
8: | a__tail(cons(X,L)) | → mark(L) | |
9: | mark(incr(X)) | → a__incr(mark(X)) | |
10: | mark(adx(X)) | → a__adx(mark(X)) | |
11: | mark(nats) | → a__nats | |
12: | mark(zeros) | → a__zeros | |
13: | mark(head(X)) | → a__head(mark(X)) | |
14: | mark(tail(X)) | → a__tail(mark(X)) | |
15: | mark(nil) | → nil | |
16: | mark(cons(X1,X2)) | → cons(mark(X1),X2) | |
17: | mark(s(X)) | → s(mark(X)) | |
18: | mark(0) | → 0 | |
19: | a__incr(X) | → incr(X) | |
20: | a__adx(X) | → adx(X) | |
21: | a__nats | → nats | |
22: | a__zeros | → zeros | |
23: | a__head(X) | → head(X) | |
24: | a__tail(X) | → tail(X) | |
25: | A__INCR(cons(X,L)) | → MARK(X) | |
26: | A__ADX(cons(X,L)) | → A__INCR(cons(mark(X),adx(L))) | |
27: | A__ADX(cons(X,L)) | → MARK(X) | |
28: | A__NATS | → A__ADX(a__zeros) | |
29: | A__NATS | → A__ZEROS | |
30: | A__HEAD(cons(X,L)) | → MARK(X) | |
31: | A__TAIL(cons(X,L)) | → MARK(L) | |
32: | MARK(incr(X)) | → A__INCR(mark(X)) | |
33: | MARK(incr(X)) | → MARK(X) | |
34: | MARK(adx(X)) | → A__ADX(mark(X)) | |
35: | MARK(adx(X)) | → MARK(X) | |
36: | MARK(nats) | → A__NATS | |
37: | MARK(zeros) | → A__ZEROS | |
38: | MARK(head(X)) | → A__HEAD(mark(X)) | |
39: | MARK(head(X)) | → MARK(X) | |
40: | MARK(tail(X)) | → A__TAIL(mark(X)) | |
41: | MARK(tail(X)) | → MARK(X) | |
42: | MARK(cons(X1,X2)) | → MARK(X1) | |
43: | MARK(s(X)) | → MARK(X) | |